PRISM
=====
Version: 4.5.dev
Date: Sat Apr 03 02:34:24 CEST 2021
Hostname: christopher
Memory limits: cudd=4g, java(heap)=11g
Command line: prism -javamaxmem 11g -cuddmaxmem 4g -heuristic speed -e 1e-6 -maxiters 1000000 rabin.20.prism rabin.20.props --property live
Parsing model file "rabin.20.prism"...
Type: MDP
Modules: process1 process2 process3 process4 process5 process6 process7 process8 process9 process10 process11 process12 process13 process14 process15 process16 process17 process18 process19 process20
Variables: c b r p1 b1 r1 draw1 p2 b2 r2 draw2 p3 b3 r3 draw3 p4 b4 r4 draw4 p5 b5 r5 draw5 p6 b6 r6 draw6 p7 b7 r7 draw7 p8 b8 r8 draw8 p9 b9 r9 draw9 p10 b10 r10 draw10 p11 b11 r11 draw11 p12 b12 r12 draw12 p13 b13 r13 draw13 p14 b14 r14 draw14 p15 b15 r15 draw15 p16 b16 r16 draw16 p17 b17 r17 draw17 p18 b18 r18 draw18 p19 b19 r19 draw19 p20 b20 r20 draw20
Parsing properties file "rabin.20.props"...
1 property:
(1) "live": Pmax=? [ F (p1=2|p2=2|p3=2|p4=2|p5=2|p6=2|p7=2|p8=2|p9=2|p10=2|p11=2|p12=2|p13=2|p14=2|p15=2|p16=2|p17=2|p18=2|p19=2|p20=2) ]
---------------------------------------------------------------------
Model checking: "live": Pmax=? [ F (p1=2|p2=2|p3=2|p4=2|p5=2|p6=2|p7=2|p8=2|p9=2|p10=2|p11=2|p12=2|p13=2|p14=2|p15=2|p16=2|p17=2|p18=2|p19=2|p20=2) ]
Warning: Switching to sparse engine and (backwards) Gauss Seidel (default for heuristic=speed).
Building model...
Computing reachable states...
Reachability (BFS): 72 iterations in 893.37 seconds (average 12.407958, setup 0.00)
Time for model construction: 910.104 seconds.
Type: MDP
States: 4.162453015158186E28 (1 initial)
Transitions: 3.962705109947689E29
Choices: 8.362648841646327E28
Transition matrix: 4167112 nodes (10 terminal), 3.962705109947689E29 minterms, vars: 186r/186c/20nd
Warning: Switching to MTBDD engine, as number of states is too large for Sparse engine.
Prob0A: 5 iterations in 4.54 seconds (average 0.909000, setup 0.00)
Prob1E: 6 iterations in 2.12 seconds (average 0.353500, setup 0.00)
yes = 4.162453015158186E28, no = 0, maybe = 0
Value in the initial state: 1.0
Time for model checking: 7.922 seconds.
Result: 1.0 (value in the initial state)
Overall running time: 918.584 seconds.
---------------------------------------------------------------------
Note: There were 2 warnings during computation.